Nuprl Lemma : es-x-equiv_wf
0,22
postcript
pdf
es
:ES,
i
,
x
:Id,
s1
,
s2
:(
x
:Id
vartype(
i
;
x
)).
s1
s2
mod
x
@
i
Prop
latex
Definitions
ES
,
t
T
,
Id
,
x
:
A
.
B
(
x
)
,
vartype(
i
;
x
)
,
x
:
A
B
(
x
)
,
f
(
a
)
,
s
=
t
,
Prop
,
A
,
P
Q
,
s1
s2
mod
x
@
i
Lemmas
not
wf
,
es-vartype
wf
,
Id
wf
,
event
system
wf
origin
es:ES, i, x:Id, s1, s2:(x:Id
vartype(i;x)). s1 
s2 mod x@i 
Prop es:ES, i, x:Id, s1, s2:(x:Idvartype(i;x)). s1 s2 mod x@i Prop Tx:A. B(x)B(x)
A
Q s2 mod x@i